T:Type, op:(TTT), id:T, inv:(TT).
Assoc(T;op)  Ident(T;op;id)  Inverse(T;op;id;inv)  (mk_igrp(T;op;id;inv)  IGroup) 

latex

Up	groups 1
Definitions of Statement	|g|, *, e, ~, IMonoid, IGroup, mk_igrp(T;op;id;inv)
Definitions	mk_igrp(T;op;id;inv), t  T, P  Q, x:A. B(x), IGroup, t.2, t.1, ~, e, *, |g|, , IMonoid
Lemmas	assoc wf, ident wf, inverse wf, grp inv wf, grp id wf, grp op wf, grp car wf, btrue wf, mk imon